\begin{tabbing}
$\forall$${\it es}$:ES, $i$, $a$, ${\it done}$:Id.
\\[0ex]@$i$ ${\it done}$ initially ff:$\mathbb{B}$
\\[0ex]$\Rightarrow$ @$i$ only [locl($a$)] affect ${\it done}$:$\mathbb{B}$
\\[0ex]$\Rightarrow$ @$i$ events of kind locl($a$) change ${\it done}$ to $\lambda$$s$,$v$. tt State(${\it done}$ : $\mathbb{B}$) (val:Unit)
\\[0ex]$\Rightarrow$ @$i$ \=Precondition for $a$(Outcome($\ast$1$\ast$)) \+
\\[0ex]$\lambda$$s$.$\neg_{b}$($s$(${\it done}$)) discrete state(${\it done}$ : $\mathbb{B}$)
\-\\[0ex]$\Rightarrow$ \=($\forall$$e$@$i$. $\forall$${\it e'}$@$i$. (kind($e$) = locl($a$) $\in$ Knd) $\Rightarrow$ (kind(${\it e'}$) = locl($a$) $\in$ Knd) $\Rightarrow$ ($e$ = ${\it e'}$ $\in$ E)\+
\\[0ex]\& $\exists$$e$@$i$.kind($e$) = locl($a$) $\in$ Knd)
\-
\end{tabbing}